Left Termination proof of /tmp/tmp

Left Termination of the query pattern
shapes(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)

↳2 TRIPLES

↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)

↳4 TRIPLES

↳5 TriplesToPiDPProof (⇒, 307 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇒, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 4 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPOrderProof (⇔, 206 ms)

        ↳22 QDP

        ↳23 DependencyGraphProof (⇔, 0 ms)

        ↳24 TRUE

    ↳25 PiDP

        ↳26 UsableRulesProof (⇔, 0 ms)

        ↳27 PiDP

        ↳28 PiDPToQDPProof (⇒, 0 ms)

        ↳29 QDP

        ↳30 QDPSizeChangeProof (⇔, 0 ms)

        ↳31 YES

    ↳32 PiDP

        ↳33 UsableRulesProof (⇔, 0 ms)

        ↳34 PiDP

        ↳35 PiDPToQDPProof (⇒, 0 ms)

        ↳36 QDP

        ↳37 QDPSizeChangeProof (⇔, 0 ms)

        ↳38 YES

(0) Obligation:

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X1), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X2, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X3, []), .(X4, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X5)).
unif(w(X6), black).

Query: shapes(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="H: shapes(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: shapes(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(varmat(T5, X11), unif_matrx(X11))\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 1 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: unif_matrx([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: unif_matrx([]), SCOPE: 3, CLAUSE: 5 | unif_matrx([]), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: unif_matrx([]), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(','(varmat(T15, X47), varmat(T16, X48)), unif_matrx(.(X47, X48)))\n\nT15 is ground\nT16 is ground\nX47 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="A: varmat(T15, X47)\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="F: ','(varmat(T16, X48), unif_matrx(.(T17, X48)))\n\nT16 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: varmat(T15, X47), SCOPE: 4, CLAUSE: 1 | varmat(T15, X47), SCOPE: 4, CLAUSE: 2 | varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: varmat(T15, X47), SCOPE: 4, CLAUSE: 1\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: varmat(T15, X47), SCOPE: 4, CLAUSE: 2 | varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: varmat(T15, X47), SCOPE: 4, CLAUSE: 2\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(varmat(T26, X77), varmat(T27, X78))\n\nT26 is ground\nT27 is ground\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: varmat(T26, X77)\n\nT26 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: varmat(T27, X78)\n\nT27 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: varmat(T15, X47), SCOPE: 4, CLAUSE: 3\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: varmat(T33, X93)\n\nT33 is ground\nX93 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: varmat(T36, X108)\n\nT36 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: varmat(T16, X48)\n\nT16 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="B: unif_matrx(.(T17, T37))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 5 | unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(unif_lines(T56, T57), unif_matrx(.(T57, T58)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="C: unif_lines(T56, T57)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: unif_matrx(.(T65, T66))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 7 | unif_lines(T56, T57), SCOPE: 6, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(unif_pairs(.(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))))), unif_lines(.(T104, T107), .(T106, T108)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="D: ','(unif_pairs(.(T103, T109)), unif_lines(.(T104, T107), .(T106, T108)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="G: unif_pairs(.(T103, T109))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: unif_lines(.(T110, T111), .(T112, T113))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 9 | unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(unif(T123, T124), unif_pairs(T125))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 11 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="E: unif_pairs(T131)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: unif_pairs(T131), SCOPE: 9, CLAUSE: 9 | unif_pairs(T131), SCOPE: 9, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: unif_pairs(T131), SCOPE: 9, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: unif_pairs(T131), SCOPE: 9, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(unif(T141, T142), unif_pairs(T143))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 11 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: unif_pairs(T149)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: unif_pairs(T150)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: unif_pairs(T156)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: unif_pairs(T160)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: unif_pairs(T161)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: unif_pairs(T167)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: unif_pairs(T171)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(varmat(T194, X245), unif_matrx(.(black, X245)))\n\nT194 is ground\nX245 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: varmat(T194, X245)\n\nT194 is ground\nX245 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: unif_matrx(.(black, T195))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 5 | unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(unif_lines(black, T208), unif_matrx(.(T208, T209)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="I: unif_lines(black, T208)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: unif_matrx(.(T210, T211))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: unif_lines(black, T208), SCOPE: 12, CLAUSE: 7 | unif_lines(black, T208), SCOPE: 12, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: unif_lines(black, T208), SCOPE: 12, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(varmat(T217, X304), unif_matrx(.(w(X303), X304)))\n\nT217 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 122 [arrowhead = none ];
122 -> 2;

123 [label="ONLY EVAL with clause\nshapes(X9, X10) :- ','(varmat(X9, X11), unif_matrx(X11)).\nand substitutionT1 -> T5,\nX9 -> T5,\nT2 -> T6,\nX10 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 123 [arrowhead = none ];
123 -> 3;

124 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 124 [arrowhead = none ];
124 -> 4;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 125 [arrowhead = none ];
125 -> 5;

126 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 126 [arrowhead = none ];
126 -> 6;

127 [label="EVAL with clause\nvarmat([], []).\nand substitutionT5 -> [],\nX11 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 127 [arrowhead = none ];
127 -> 7;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 128 [arrowhead = none ];
128 -> 8;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 129 [arrowhead = none ];
129 -> 12;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 130 [arrowhead = none ];
130 -> 13;

131 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 131 [arrowhead = none ];
131 -> 9;

132 [label="BACKTRACK\nfor clause: unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 132 [arrowhead = none ];
132 -> 10;

133 [label="BACKTRACK\nfor clause: unif_matrx(.(X2, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 133 [arrowhead = none ];
133 -> 11;

134 [label="EVAL with clause\nvarmat(.(X43, X44), .(X45, X46)) :- ','(varmat(X43, X45), varmat(X44, X46)).\nand substitutionX43 -> T15,\nX44 -> T16,\nT5 -> .(T15, T16),\nX45 -> X47,\nX46 -> X48,\nX11 -> .(X47, X48)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 134 [arrowhead = none ];
134 -> 14;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 135 [arrowhead = none ];
135 -> 15;

136 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 136 [arrowhead = none ];
136 -> 101;

137 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 137 [arrowhead = none ];
137 -> 102;

138 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 138 [arrowhead = none ];
138 -> 16;

139 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nreplacements:X47 -> T17", fontsize=14, style = filled, fillcolor = violet];
14 -> 139 [arrowhead = none ];
139 -> 17;

140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 140 [arrowhead = none ];
140 -> 18;

141 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 141 [arrowhead = none ];
141 -> 36;

142 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nreplacements:X48 -> T37", fontsize=14, style = filled, fillcolor = violet];
17 -> 142 [arrowhead = none ];
142 -> 37;

143 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 143 [arrowhead = none ];
143 -> 19;

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 144 [arrowhead = none ];
144 -> 20;

145 [label="EVAL with clause\nvarmat([], []).\nand substitutionT15 -> [],\nX47 -> []", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 145 [arrowhead = none ];
145 -> 21;

146 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 146 [arrowhead = none ];
146 -> 22;

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 147 [arrowhead = none ];
147 -> 24;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 148 [arrowhead = none ];
148 -> 25;

149 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 149 [arrowhead = none ];
149 -> 23;

150 [label="EVAL with clause\nvarmat(.(X73, X74), .(X75, X76)) :- ','(varmat(X73, X75), varmat(X74, X76)).\nand substitutionX73 -> T26,\nX74 -> T27,\nT15 -> .(T26, T27),\nX75 -> X77,\nX76 -> X78,\nX47 -> .(X77, X78)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 150 [arrowhead = none ];
150 -> 26;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 151 [arrowhead = none ];
151 -> 27;

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
25 -> 152 [arrowhead = none ];
152 -> 30;

153 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
25 -> 153 [arrowhead = none ];
153 -> 31;

154 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
26 -> 154 [arrowhead = none ];
154 -> 28;

155 [label="SPLIT 2\nnew knowledge:\nT26 is ground\nreplacements:X77 -> T28", fontsize=14, style = filled, fillcolor = violet];
26 -> 155 [arrowhead = none ];
155 -> 29;

156 [label="INSTANCE with matching:\nT15 -> T26\nX47 -> X77", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 156 [arrowhead = none , style=dashed];
156 -> 16[style=dashed];

157 [label="INSTANCE with matching:\nT15 -> T27\nX47 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
29 -> 157 [arrowhead = none , style=dashed];
157 -> 16[style=dashed];

158 [label="EVAL with clause\nvarmat(.(black, X91), .(black, X92)) :- varmat(X91, X92).\nand substitutionX91 -> T33,\nT15 -> .(black, T33),\nX92 -> X93,\nX47 -> .(black, X93)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 158 [arrowhead = none ];
158 -> 32;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 159 [arrowhead = none ];
159 -> 33;

160 [label="EVAL with clause\nvarmat(.(white, X104), .(w(X105), X106)) :- varmat(X104, X106).\nand substitutionX104 -> T36,\nT15 -> .(white, T36),\nX105 -> X107,\nX106 -> X108,\nX47 -> .(w(X107), X108)", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 160 [arrowhead = none ];
160 -> 34;

161 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 161 [arrowhead = none ];
161 -> 35;

162 [label="INSTANCE with matching:\nT15 -> T33\nX47 -> X93", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 162 [arrowhead = none , style=dashed];
162 -> 16[style=dashed];

163 [label="INSTANCE with matching:\nT15 -> T36\nX47 -> X108", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 163 [arrowhead = none , style=dashed];
163 -> 16[style=dashed];

164 [label="INSTANCE with matching:\nT15 -> T16\nX47 -> X48", fontsize=14, style = filled, fillcolor = lightgrey];
36 -> 164 [arrowhead = none , style=dashed];
164 -> 16[style=dashed];

165 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 165 [arrowhead = none ];
165 -> 38;

166 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 166 [arrowhead = none ];
166 -> 39;

167 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 167 [arrowhead = none ];
167 -> 40;

168 [label="EVAL with clause\nunif_matrx(.(X124, .(X125, X126))) :- ','(unif_lines(X124, X125), unif_matrx(.(X125, X126))).\nand substitutionT17 -> T56,\nX124 -> T56,\nX125 -> T57,\nX126 -> T58,\nT37 -> .(T57, T58),\nT53 -> T56,\nT54 -> T57,\nT55 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 168 [arrowhead = none ];
168 -> 41;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 169 [arrowhead = none ];
169 -> 42;

170 [label="EVAL with clause\nunif_matrx(.(X230, [])).\nand substitutionT17 -> T189,\nX230 -> T189,\nT37 -> []", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 170 [arrowhead = none ];
170 -> 98;

171 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 171 [arrowhead = none ];
171 -> 99;

172 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
41 -> 172 [arrowhead = none ];
172 -> 43;

173 [label="SPLIT 2\nreplacements:T57 -> T65,\nT58 -> T66", fontsize=14, style = filled, fillcolor = violet];
41 -> 173 [arrowhead = none ];
173 -> 44;

174 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 174 [arrowhead = none ];
174 -> 45;

175 [label="INSTANCE with matching:\nT17 -> T65\nT37 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 175 [arrowhead = none , style=dashed];
175 -> 37[style=dashed];

176 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 176 [arrowhead = none ];
176 -> 46;

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 177 [arrowhead = none ];
177 -> 47;

178 [label="EVAL with clause\nunif_lines(.(X163, .(X164, X165)), .(X166, .(X167, X168))) :- ','(unif_pairs(.(X163, .(X164, .(X166, .(X167, .(X163, .(X166, .(X164, .(X167, .(X163, .(X167, .(X164, .(X166, []))))))))))))), unif_lines(.(X164, X165), .(X167, X168))).\nand substitutionX163 -> T103,\nX164 -> T104,\nX165 -> T107,\nT56 -> .(T103, .(T104, T107)),\nX166 -> T105,\nX167 -> T106,\nX168 -> T108,\nT57 -> .(T105, .(T106, T108)),\nT97 -> T103,\nT98 -> T104,\nT100 -> T105,\nT101 -> T106,\nT99 -> T107,\nT102 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 178 [arrowhead = none ];
178 -> 48;

179 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 179 [arrowhead = none ];
179 -> 49;

180 [label="EVAL with clause\nunif_lines(.(X223, []), .(X224, [])).\nand substitutionX223 -> T182,\nT56 -> .(T182, []),\nX224 -> T183,\nT57 -> .(T183, [])", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 180 [arrowhead = none ];
180 -> 95;

181 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 181 [arrowhead = none ];
181 -> 96;

182 [label="GENERALIZATION\nT109 <-- .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, [])))))))))))", fontsize=14, style = filled, fillcolor = violet];
48 -> 182 [arrowhead = none ];
182 -> 50;

183 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
50 -> 183 [arrowhead = none ];
183 -> 51;

184 [label="SPLIT 2\nreplacements:T104 -> T110,\nT107 -> T111,\nT106 -> T112,\nT108 -> T113", fontsize=14, style = filled, fillcolor = violet];
50 -> 184 [arrowhead = none ];
184 -> 52;

185 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 185 [arrowhead = none ];
185 -> 53;

186 [label="INSTANCE with matching:\nT56 -> .(T110, T111)\nT57 -> .(T112, T113)", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 186 [arrowhead = none , style=dashed];
186 -> 43[style=dashed];

187 [label="BACKTRACK\nfor clause: unif_pairs([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 187 [arrowhead = none ];
187 -> 54;

188 [label="EVAL with clause\nunif_pairs(.(X175, .(X176, X177))) :- ','(unif(X175, X176), unif_pairs(X177)).\nand substitutionT103 -> T123,\nX175 -> T123,\nX176 -> T124,\nX177 -> T125,\nT109 -> .(T124, T125),\nT120 -> T123,\nT121 -> T124,\nT122 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 188 [arrowhead = none ];
188 -> 55;

189 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 189 [arrowhead = none ];
189 -> 56;

190 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 190 [arrowhead = none ];
190 -> 57;

191 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
57 -> 191 [arrowhead = none ];
191 -> 58;

192 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
57 -> 192 [arrowhead = none ];
192 -> 59;

193 [label="EVAL with clause\nunif(w(X182), w(X182)).\nand substitutionX182 -> T130,\nT123 -> w(T130),\nT124 -> w(T130),\nT125 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 193 [arrowhead = none ];
193 -> 60;

194 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 194 [arrowhead = none ];
194 -> 61;

195 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
59 -> 195 [arrowhead = none ];
195 -> 85;

196 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
59 -> 196 [arrowhead = none ];
196 -> 86;

197 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 197 [arrowhead = none ];
197 -> 62;

198 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 198 [arrowhead = none ];
198 -> 63;

199 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 199 [arrowhead = none ];
199 -> 64;

200 [label="EVAL with clause\nunif_pairs([]).\nand substitutionT131 -> []", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 200 [arrowhead = none ];
200 -> 65;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 201 [arrowhead = none ];
201 -> 66;

202 [label="EVAL with clause\nunif_pairs(.(X189, .(X190, X191))) :- ','(unif(X189, X190), unif_pairs(X191)).\nand substitutionX189 -> T141,\nX190 -> T142,\nX191 -> T143,\nT131 -> .(T141, .(T142, T143)),\nT138 -> T141,\nT139 -> T142,\nT140 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 202 [arrowhead = none ];
202 -> 68;

203 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 203 [arrowhead = none ];
203 -> 69;

204 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 204 [arrowhead = none ];
204 -> 67;

205 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 205 [arrowhead = none ];
205 -> 70;

206 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 206 [arrowhead = none ];
206 -> 71;

207 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 207 [arrowhead = none ];
207 -> 72;

208 [label="EVAL with clause\nunif(w(X196), w(X196)).\nand substitutionX196 -> T148,\nT141 -> w(T148),\nT142 -> w(T148),\nT143 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 208 [arrowhead = none ];
208 -> 73;

209 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 209 [arrowhead = none ];
209 -> 74;

210 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
72 -> 210 [arrowhead = none ];
210 -> 75;

211 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
72 -> 211 [arrowhead = none ];
211 -> 76;

212 [label="INSTANCE with matching:\nT131 -> T149", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 212 [arrowhead = none , style=dashed];
212 -> 60[style=dashed];

213 [label="EVAL with clause\nunif(black, black).\nand substitutionT141 -> black,\nT142 -> black,\nT143 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 213 [arrowhead = none ];
213 -> 77;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 214 [arrowhead = none ];
214 -> 78;

215 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 215 [arrowhead = none ];
215 -> 79;

216 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 216 [arrowhead = none ];
216 -> 80;

217 [label="INSTANCE with matching:\nT131 -> T150", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 217 [arrowhead = none , style=dashed];
217 -> 60[style=dashed];

218 [label="EVAL with clause\nunif(black, w(X201)).\nand substitutionT141 -> black,\nX201 -> T155,\nT142 -> w(T155),\nT143 -> T156", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 218 [arrowhead = none ];
218 -> 81;

219 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 219 [arrowhead = none ];
219 -> 82;

220 [label="EVAL with clause\nunif(w(X204), black).\nand substitutionX204 -> T159,\nT141 -> w(T159),\nT142 -> black,\nT143 -> T160", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 220 [arrowhead = none ];
220 -> 83;

221 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 221 [arrowhead = none ];
221 -> 84;

222 [label="INSTANCE with matching:\nT131 -> T156", fontsize=14, style = filled, fillcolor = lightgrey];
81 -> 222 [arrowhead = none , style=dashed];
222 -> 60[style=dashed];

223 [label="INSTANCE with matching:\nT131 -> T160", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 223 [arrowhead = none , style=dashed];
223 -> 60[style=dashed];

224 [label="EVAL with clause\nunif(black, black).\nand substitutionT123 -> black,\nT124 -> black,\nT125 -> T161", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 224 [arrowhead = none ];
224 -> 87;

225 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 225 [arrowhead = none ];
225 -> 88;

226 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
86 -> 226 [arrowhead = none ];
226 -> 89;

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
86 -> 227 [arrowhead = none ];
227 -> 90;

228 [label="INSTANCE with matching:\nT131 -> T161", fontsize=14, style = filled, fillcolor = lightgrey];
87 -> 228 [arrowhead = none , style=dashed];
228 -> 60[style=dashed];

229 [label="EVAL with clause\nunif(black, w(X209)).\nand substitutionT123 -> black,\nX209 -> T166,\nT124 -> w(T166),\nT125 -> T167", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 229 [arrowhead = none ];
229 -> 91;

230 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 230 [arrowhead = none ];
230 -> 92;

231 [label="EVAL with clause\nunif(w(X212), black).\nand substitutionX212 -> T170,\nT123 -> w(T170),\nT124 -> black,\nT125 -> T171", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 231 [arrowhead = none ];
231 -> 93;

232 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 232 [arrowhead = none ];
232 -> 94;

233 [label="INSTANCE with matching:\nT131 -> T167", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 233 [arrowhead = none , style=dashed];
233 -> 60[style=dashed];

234 [label="INSTANCE with matching:\nT131 -> T171", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 234 [arrowhead = none , style=dashed];
234 -> 60[style=dashed];

235 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 235 [arrowhead = none ];
235 -> 97;

236 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 236 [arrowhead = none ];
236 -> 100;

237 [label="EVAL with clause\nvarmat(.(black, X243), .(black, X244)) :- varmat(X243, X244).\nand substitutionX243 -> T194,\nT5 -> .(black, T194),\nX244 -> X245,\nX11 -> .(black, X245)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 237 [arrowhead = none ];
237 -> 103;

238 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 238 [arrowhead = none ];
238 -> 104;

239 [label="EVAL with clause\nvarmat(.(white, X300), .(w(X301), X302)) :- varmat(X300, X302).\nand substitutionX300 -> T217,\nT5 -> .(white, T217),\nX301 -> X303,\nX302 -> X304,\nX11 -> .(w(X303), X304)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 239 [arrowhead = none ];
239 -> 120;

240 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 240 [arrowhead = none ];
240 -> 121;

241 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
103 -> 241 [arrowhead = none ];
241 -> 105;

242 [label="SPLIT 2\nnew knowledge:\nT194 is ground\nreplacements:X245 -> T195", fontsize=14, style = filled, fillcolor = violet];
103 -> 242 [arrowhead = none ];
242 -> 106;

243 [label="INSTANCE with matching:\nT15 -> T194\nX47 -> X245", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 243 [arrowhead = none , style=dashed];
243 -> 16[style=dashed];

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 244 [arrowhead = none ];
244 -> 107;

245 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 245 [arrowhead = none ];
245 -> 108;

246 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 246 [arrowhead = none ];
246 -> 109;

247 [label="EVAL with clause\nunif_matrx(.(X261, .(X262, X263))) :- ','(unif_lines(X261, X262), unif_matrx(.(X262, X263))).\nand substitutionX261 -> black,\nX262 -> T208,\nX263 -> T209,\nT195 -> .(T208, T209),\nT206 -> T208,\nT207 -> T209", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 247 [arrowhead = none ];
247 -> 110;

248 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 248 [arrowhead = none ];
248 -> 111;

249 [label="EVAL with clause\nunif_matrx(.(X289, [])).\nand substitutionX289 -> black,\nT195 -> []", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 249 [arrowhead = none ];
249 -> 117;

250 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 250 [arrowhead = none ];
250 -> 118;

251 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 251 [arrowhead = none ];
251 -> 112;

252 [label="SPLIT 2\nreplacements:T208 -> T210,\nT209 -> T211", fontsize=14, style = filled, fillcolor = violet];
110 -> 252 [arrowhead = none ];
252 -> 113;

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
112 -> 253 [arrowhead = none ];
253 -> 114;

254 [label="INSTANCE with matching:\nT17 -> T210\nT37 -> T211", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 254 [arrowhead = none , style=dashed];
254 -> 37[style=dashed];

255 [label="BACKTRACK\nfor clause: unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 255 [arrowhead = none ];
255 -> 115;

256 [label="BACKTRACK\nfor clause: unif_lines(.(X3, []), .(X4, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 256 [arrowhead = none ];
256 -> 116;

257 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 257 [arrowhead = none ];
257 -> 119;

258 [label="INSTANCE with matching:\nT16 -> T217\nX48 -> X304\nT17 -> w(X303)", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 258 [arrowhead = none , style=dashed];
258 -> 17[style=dashed];

}

(2) Obligation:

Triples:

varmatA(.(X1, X2), .(X3, X4)) :- varmatA(X1, X3).
varmatA(.(X1, X2), .(X3, X4)) :- ','(varmatcA(X1, X3), varmatA(X2, X4)).
varmatA(.(black, X1), .(black, X2)) :- varmatA(X1, X2).
varmatA(.(white, X1), .(w(X2), X3)) :- varmatA(X1, X3).
unif_matrxB(X1, .(X2, X3)) :- unif_linesC(X1, X2).
unif_matrxB(X1, .(X2, X3)) :- ','(unif_linescC(X1, X2), unif_matrxB(X2, X3)).
unif_linesC(.(X1, .(X2, X3)), .(X4, .(X5, X6))) :- pD(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6).
unif_pairsE(.(w(X1), .(w(X1), X2))) :- unif_pairsE(X2).
unif_pairsE(.(black, .(black, X1))) :- unif_pairsE(X1).
unif_pairsE(.(black, .(w(X1), X2))) :- unif_pairsE(X2).
unif_pairsE(.(w(X1), .(black, X2))) :- unif_pairsE(X2).
pF(X1, X2, X3) :- varmatA(X1, X2).
pF(X1, X2, X3) :- ','(varmatcA(X1, X2), unif_matrxB(X3, X2)).
pD(w(X1), .(w(X1), X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(black, .(black, X1), X2, X3, X4, X5) :- unif_pairsE(X1).
pD(black, .(w(X1), X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(w(X1), .(black, X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(X1, X2, X3, X4, X5, X6) :- ','(unif_pairscG(X1, X2), unif_linesC(.(X3, X4), .(X5, X6))).
shapesH(.(X1, X2), X3) :- varmatA(X1, X4).
shapesH(.(X1, X2), X3) :- ','(varmatcA(X1, X4), pF(X2, X5, X4)).
shapesH(.(black, X1), X2) :- varmatA(X1, X3).
shapesH(.(black, X1), X2) :- ','(varmatcA(X1, .(X3, X4)), ','(unif_linescI(X3), unif_matrxB(X3, X4))).
shapesH(.(white, X1), X2) :- pF(X1, X3, w(X4)).

Clauses:

varmatcA([], []).
varmatcA(.(X1, X2), .(X3, X4)) :- ','(varmatcA(X1, X3), varmatcA(X2, X4)).
varmatcA(.(black, X1), .(black, X2)) :- varmatcA(X1, X2).
varmatcA(.(white, X1), .(w(X2), X3)) :- varmatcA(X1, X3).
unif_matrxcB(X1, .(X2, X3)) :- ','(unif_linescC(X1, X2), unif_matrxcB(X2, X3)).
unif_matrxcB(X1, []).
unif_linescC(.(X1, .(X2, X3)), .(X4, .(X5, X6))) :- qcD(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6).
unif_linescC(.(X1, []), .(X2, [])).
unif_pairscE([]).
unif_pairscE(.(w(X1), .(w(X1), X2))) :- unif_pairscE(X2).
unif_pairscE(.(black, .(black, X1))) :- unif_pairscE(X1).
unif_pairscE(.(black, .(w(X1), X2))) :- unif_pairscE(X2).
unif_pairscE(.(w(X1), .(black, X2))) :- unif_pairscE(X2).
qcF(X1, X2, X3) :- ','(varmatcA(X1, X2), unif_matrxcB(X3, X2)).
qcD(X1, X2, X3, X4, X5, X6) :- ','(unif_pairscG(X1, X2), unif_linescC(.(X3, X4), .(X5, X6))).
unif_pairscG(w(X1), .(w(X1), X2)) :- unif_pairscE(X2).
unif_pairscG(black, .(black, X1)) :- unif_pairscE(X1).
unif_pairscG(black, .(w(X1), X2)) :- unif_pairscE(X2).
unif_pairscG(w(X1), .(black, X2)) :- unif_pairscE(X2).

Afs:

shapesH(x1, x2) = shapesH(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

varmatA(.(X1, X2), .(X3, X4)) :- varmatA(X1, X3).
varmatA(.(X1, X2), .(X3, X4)) :- ','(varmatcA(X1, X3), varmatA(X2, X4)).
varmatA(.(black, X1), .(black, X2)) :- varmatA(X1, X2).
varmatA(.(white, X1), .(w(X2), X3)) :- varmatA(X1, X3).
unif_matrxB(X1, .(X2, X3)) :- unif_linesC(X1, X2).
unif_matrxB(X1, .(X2, X3)) :- ','(unif_linescC(X1, X2), unif_matrxB(X2, X3)).
unif_linesC(.(X1, .(X2, X3)), .(X4, .(X5, X6))) :- pD(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6).
unif_pairsE(.(w(X1), .(w(X1), X2))) :- unif_pairsE(X2).
unif_pairsE(.(black, .(black, X1))) :- unif_pairsE(X1).
unif_pairsE(.(black, .(w(X1), X2))) :- unif_pairsE(X2).
unif_pairsE(.(w(X1), .(black, X2))) :- unif_pairsE(X2).
pF(X1, X2, X3) :- varmatA(X1, X2).
pF(X1, X2, X3) :- ','(varmatcA(X1, X2), unif_matrxB(X3, X2)).
pD(w(X1), .(w(X1), X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(black, .(black, X1), X2, X3, X4, X5) :- unif_pairsE(X1).
pD(black, .(w(X1), X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(w(X1), .(black, X2), X3, X4, X5, X6) :- unif_pairsE(X2).
pD(X1, X2, X3, X4, X5, X6) :- ','(unif_pairscG(X1, X2), unif_linesC(.(X3, X4), .(X5, X6))).
shapesH(.(X1, X2), X3) :- varmatA(X1, X4).
shapesH(.(X1, X2), X3) :- ','(varmatcA(X1, X4), pF(X2, X5, X4)).
shapesH(.(black, X1), X2) :- varmatA(X1, X3).
shapesH(.(white, X1), X2) :- pF(X1, X3, w(X4)).

Clauses:

varmatcA([], []).
varmatcA(.(X1, X2), .(X3, X4)) :- ','(varmatcA(X1, X3), varmatcA(X2, X4)).
varmatcA(.(black, X1), .(black, X2)) :- varmatcA(X1, X2).
varmatcA(.(white, X1), .(w(X2), X3)) :- varmatcA(X1, X3).
unif_matrxcB(X1, .(X2, X3)) :- ','(unif_linescC(X1, X2), unif_matrxcB(X2, X3)).
unif_matrxcB(X1, []).
unif_linescC(.(X1, .(X2, X3)), .(X4, .(X5, X6))) :- qcD(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6).
unif_linescC(.(X1, []), .(X2, [])).
unif_pairscE([]).
unif_pairscE(.(w(X1), .(w(X1), X2))) :- unif_pairscE(X2).
unif_pairscE(.(black, .(black, X1))) :- unif_pairscE(X1).
unif_pairscE(.(black, .(w(X1), X2))) :- unif_pairscE(X2).
unif_pairscE(.(w(X1), .(black, X2))) :- unif_pairscE(X2).
qcF(X1, X2, X3) :- ','(varmatcA(X1, X2), unif_matrxcB(X3, X2)).
qcD(X1, X2, X3, X4, X5, X6) :- ','(unif_pairscG(X1, X2), unif_linescC(.(X3, X4), .(X5, X6))).
unif_pairscG(w(X1), .(w(X1), X2)) :- unif_pairscE(X2).
unif_pairscG(black, .(black, X1)) :- unif_pairscE(X1).
unif_pairscG(black, .(w(X1), X2)) :- unif_pairscE(X2).
unif_pairscG(w(X1), .(black, X2)) :- unif_pairscE(X2).

Afs:

shapesH(x1, x2) = shapesH(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
shapesH_in: (b,f)
varmatA_in: (b,f)
varmatcA_in: (b,f)
pF_in: (b,f,b)
unif_matrxB_in: (b,b)
unif_linesC_in: (b,b)
pD_in: (b,b,b,b,b,b)
unif_pairsE_in: (b)
unif_pairscG_in: (b,b)
unif_pairscE_in: (b)
unif_linescC_in: (b,b)
qcD_in: (b,b,b,b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SHAPESH_IN_GA(.(X1, X2), X3) → U23_GA(X1, X2, X3, varmatA_in_ga(X1, X4))
SHAPESH_IN_GA(.(X1, X2), X3) → VARMATA_IN_GA(X1, X4)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U1_GA(X1, X2, X3, X4, varmatA_in_ga(X1, X3))
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → VARMATA_IN_GA(X1, X3)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U2_GA(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U3_GA(X1, X2, X3, X4, varmatA_in_ga(X2, X4))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2, X4)
VARMATA_IN_GA(.(black, X1), .(black, X2)) → U4_GA(X1, X2, varmatA_in_ga(X1, X2))
VARMATA_IN_GA(.(black, X1), .(black, X2)) → VARMATA_IN_GA(X1, X2)
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → U5_GA(X1, X2, X3, varmatA_in_ga(X1, X3))
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → VARMATA_IN_GA(X1, X3)
SHAPESH_IN_GA(.(X1, X2), X3) → U24_GA(X1, X2, X3, varmatcA_in_ga(X1, X4))
U24_GA(X1, X2, X3, varmatcA_out_ga(X1, X4)) → U25_GA(X1, X2, X3, pF_in_gag(X2, X5, X4))
U24_GA(X1, X2, X3, varmatcA_out_ga(X1, X4)) → PF_IN_GAG(X2, X5, X4)
PF_IN_GAG(X1, X2, X3) → U14_GAG(X1, X2, X3, varmatA_in_ga(X1, X2))
PF_IN_GAG(X1, X2, X3) → VARMATA_IN_GA(X1, X2)
PF_IN_GAG(X1, X2, X3) → U15_GAG(X1, X2, X3, varmatcA_in_ga(X1, X2))
U15_GAG(X1, X2, X3, varmatcA_out_ga(X1, X2)) → U16_GAG(X1, X2, X3, unif_matrxB_in_gg(X3, X2))
U15_GAG(X1, X2, X3, varmatcA_out_ga(X1, X2)) → UNIF_MATRXB_IN_GG(X3, X2)
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U6_GG(X1, X2, X3, unif_linesC_in_gg(X1, X2))
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → UNIF_LINESC_IN_GG(X1, X2)
UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U9_GG(X1, X2, X3, X4, X5, X6, pD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)
PD_IN_GGGGGG(w(X1), .(w(X1), X2), X3, X4, X5, X6) → U17_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(w(X1), .(w(X1), X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → U10_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → U11_G(X1, unif_pairsE_in_g(X1))
UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → U12_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → U13_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(black, .(black, X1), X2, X3, X4, X5) → U18_GGGGGG(X1, X2, X3, X4, X5, unif_pairsE_in_g(X1))
PD_IN_GGGGGG(black, .(black, X1), X2, X3, X4, X5) → UNIF_PAIRSE_IN_G(X1)
PD_IN_GGGGGG(black, .(w(X1), X2), X3, X4, X5, X6) → U19_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(black, .(w(X1), X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(w(X1), .(black, X2), X3, X4, X5, X6) → U20_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(w(X1), .(black, X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U22_GGGGGG(X1, X2, X3, X4, X5, X6, unif_linesC_in_gg(.(X3, X4), .(X5, X6)))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → U8_GG(X1, X2, X3, unif_matrxB_in_gg(X2, X3))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)
SHAPESH_IN_GA(.(black, X1), X2) → U26_GA(X1, X2, varmatA_in_ga(X1, X3))
SHAPESH_IN_GA(.(black, X1), X2) → VARMATA_IN_GA(X1, X3)
SHAPESH_IN_GA(.(white, X1), X2) → U27_GA(X1, X2, pF_in_gag(X1, X3, w(X4)))
SHAPESH_IN_GA(.(white, X1), X2) → PF_IN_GAG(X1, X3, w(X4))

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatA_in_ga(x1, x2) = varmatA_in_ga(x1)
varmatcA_in_ga(x1, x2) = varmatcA_in_ga(x1)
[] = []
varmatcA_out_ga(x1, x2) = varmatcA_out_ga(x1, x2)
U29_ga(x1, x2, x3, x4, x5) = U29_ga(x1, x2, x5)
black = black
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
white = white
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
w(x1) = w
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x3, x5)
pF_in_gag(x1, x2, x3) = pF_in_gag(x1, x3)
unif_matrxB_in_gg(x1, x2) = unif_matrxB_in_gg(x1, x2)
unif_linesC_in_gg(x1, x2) = unif_linesC_in_gg(x1, x2)
pD_in_gggggg(x1, x2, x3, x4, x5, x6) = pD_in_gggggg(x1, x2, x3, x4, x5, x6)
unif_pairsE_in_g(x1) = unif_pairsE_in_g(x1)
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
SHAPESH_IN_GA(x1, x2) = SHAPESH_IN_GA(x1)
U23_GA(x1, x2, x3, x4) = U23_GA(x1, x2, x4)
VARMATA_IN_GA(x1, x2) = VARMATA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x5)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
U5_GA(x1, x2, x3, x4) = U5_GA(x1, x4)
U24_GA(x1, x2, x3, x4) = U24_GA(x1, x2, x4)
U25_GA(x1, x2, x3, x4) = U25_GA(x1, x2, x4)
PF_IN_GAG(x1, x2, x3) = PF_IN_GAG(x1, x3)
U14_GAG(x1, x2, x3, x4) = U14_GAG(x1, x3, x4)
U15_GAG(x1, x2, x3, x4) = U15_GAG(x1, x3, x4)
U16_GAG(x1, x2, x3, x4) = U16_GAG(x1, x3, x4)
UNIF_MATRXB_IN_GG(x1, x2) = UNIF_MATRXB_IN_GG(x1, x2)
U6_GG(x1, x2, x3, x4) = U6_GG(x1, x2, x3, x4)
UNIF_LINESC_IN_GG(x1, x2) = UNIF_LINESC_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4, x5, x6, x7) = U9_GG(x1, x2, x3, x4, x5, x6, x7)
PD_IN_GGGGGG(x1, x2, x3, x4, x5, x6) = PD_IN_GGGGGG(x1, x2, x3, x4, x5, x6)
U17_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U17_GGGGGG(x2, x3, x4, x5, x6, x7)
UNIF_PAIRSE_IN_G(x1) = UNIF_PAIRSE_IN_G(x1)
U10_G(x1, x2, x3) = U10_G(x2, x3)
U11_G(x1, x2) = U11_G(x1, x2)
U12_G(x1, x2, x3) = U12_G(x2, x3)
U13_G(x1, x2, x3) = U13_G(x2, x3)
U18_GGGGGG(x1, x2, x3, x4, x5, x6) = U18_GGGGGG(x1, x2, x3, x4, x5, x6)
U19_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U19_GGGGGG(x2, x3, x4, x5, x6, x7)
U20_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U20_GGGGGG(x2, x3, x4, x5, x6, x7)
U21_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U21_GGGGGG(x1, x2, x3, x4, x5, x6, x7)
U22_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U22_GGGGGG(x1, x2, x3, x4, x5, x6, x7)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x2, x3, x4)
U8_GG(x1, x2, x3, x4) = U8_GG(x1, x2, x3, x4)
U26_GA(x1, x2, x3) = U26_GA(x1, x3)
U27_GA(x1, x2, x3) = U27_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SHAPESH_IN_GA(.(X1, X2), X3) → U23_GA(X1, X2, X3, varmatA_in_ga(X1, X4))
SHAPESH_IN_GA(.(X1, X2), X3) → VARMATA_IN_GA(X1, X4)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U1_GA(X1, X2, X3, X4, varmatA_in_ga(X1, X3))
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → VARMATA_IN_GA(X1, X3)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U2_GA(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U3_GA(X1, X2, X3, X4, varmatA_in_ga(X2, X4))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2, X4)
VARMATA_IN_GA(.(black, X1), .(black, X2)) → U4_GA(X1, X2, varmatA_in_ga(X1, X2))
VARMATA_IN_GA(.(black, X1), .(black, X2)) → VARMATA_IN_GA(X1, X2)
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → U5_GA(X1, X2, X3, varmatA_in_ga(X1, X3))
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → VARMATA_IN_GA(X1, X3)
SHAPESH_IN_GA(.(X1, X2), X3) → U24_GA(X1, X2, X3, varmatcA_in_ga(X1, X4))
U24_GA(X1, X2, X3, varmatcA_out_ga(X1, X4)) → U25_GA(X1, X2, X3, pF_in_gag(X2, X5, X4))
U24_GA(X1, X2, X3, varmatcA_out_ga(X1, X4)) → PF_IN_GAG(X2, X5, X4)
PF_IN_GAG(X1, X2, X3) → U14_GAG(X1, X2, X3, varmatA_in_ga(X1, X2))
PF_IN_GAG(X1, X2, X3) → VARMATA_IN_GA(X1, X2)
PF_IN_GAG(X1, X2, X3) → U15_GAG(X1, X2, X3, varmatcA_in_ga(X1, X2))
U15_GAG(X1, X2, X3, varmatcA_out_ga(X1, X2)) → U16_GAG(X1, X2, X3, unif_matrxB_in_gg(X3, X2))
U15_GAG(X1, X2, X3, varmatcA_out_ga(X1, X2)) → UNIF_MATRXB_IN_GG(X3, X2)
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U6_GG(X1, X2, X3, unif_linesC_in_gg(X1, X2))
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → UNIF_LINESC_IN_GG(X1, X2)
UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U9_GG(X1, X2, X3, X4, X5, X6, pD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)
PD_IN_GGGGGG(w(X1), .(w(X1), X2), X3, X4, X5, X6) → U17_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(w(X1), .(w(X1), X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → U10_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → U11_G(X1, unif_pairsE_in_g(X1))
UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → U12_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → U13_G(X1, X2, unif_pairsE_in_g(X2))
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(black, .(black, X1), X2, X3, X4, X5) → U18_GGGGGG(X1, X2, X3, X4, X5, unif_pairsE_in_g(X1))
PD_IN_GGGGGG(black, .(black, X1), X2, X3, X4, X5) → UNIF_PAIRSE_IN_G(X1)
PD_IN_GGGGGG(black, .(w(X1), X2), X3, X4, X5, X6) → U19_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(black, .(w(X1), X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(w(X1), .(black, X2), X3, X4, X5, X6) → U20_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairsE_in_g(X2))
PD_IN_GGGGGG(w(X1), .(black, X2), X3, X4, X5, X6) → UNIF_PAIRSE_IN_G(X2)
PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U22_GGGGGG(X1, X2, X3, X4, X5, X6, unif_linesC_in_gg(.(X3, X4), .(X5, X6)))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → U8_GG(X1, X2, X3, unif_matrxB_in_gg(X2, X3))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)
SHAPESH_IN_GA(.(black, X1), X2) → U26_GA(X1, X2, varmatA_in_ga(X1, X3))
SHAPESH_IN_GA(.(black, X1), X2) → VARMATA_IN_GA(X1, X3)
SHAPESH_IN_GA(.(white, X1), X2) → U27_GA(X1, X2, pF_in_gag(X1, X3, w(X4)))
SHAPESH_IN_GA(.(white, X1), X2) → PF_IN_GAG(X1, X3, w(X4))

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 35 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → UNIF_PAIRSE_IN_G(X2)

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatcA_in_ga(x1, x2) = varmatcA_in_ga(x1)
[] = []
varmatcA_out_ga(x1, x2) = varmatcA_out_ga(x1, x2)
U29_ga(x1, x2, x3, x4, x5) = U29_ga(x1, x2, x5)
black = black
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
white = white
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
w(x1) = w
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x3, x5)
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
UNIF_PAIRSE_IN_G(x1) = UNIF_PAIRSE_IN_G(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
UNIF_PAIRSE_IN_G(.(w(X1), .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(black, .(w(X1), X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w(X1), .(black, X2))) → UNIF_PAIRSE_IN_G(X2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
black = black
w(x1) = w
UNIF_PAIRSE_IN_G(x1) = UNIF_PAIRSE_IN_G(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
UNIF_PAIRSE_IN_G(.(w, .(w, X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(black, .(w, X2))) → UNIF_PAIRSE_IN_G(X2)
UNIF_PAIRSE_IN_G(.(w, .(black, X2))) → UNIF_PAIRSE_IN_G(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

UNIF_PAIRSE_IN_G(.(black, .(black, X1))) → UNIF_PAIRSE_IN_G(X1)
The graph contains the following edges 1 > 1
UNIF_PAIRSE_IN_G(.(w, .(w, X2))) → UNIF_PAIRSE_IN_G(X2)
The graph contains the following edges 1 > 1
UNIF_PAIRSE_IN_G(.(black, .(w, X2))) → UNIF_PAIRSE_IN_G(X2)
The graph contains the following edges 1 > 1
UNIF_PAIRSE_IN_G(.(w, .(black, X2))) → UNIF_PAIRSE_IN_G(X2)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)
PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatcA_in_ga(x1, x2) = varmatcA_in_ga(x1)
[] = []
varmatcA_out_ga(x1, x2) = varmatcA_out_ga(x1, x2)
U29_ga(x1, x2, x3, x4, x5) = U29_ga(x1, x2, x5)
black = black
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
white = white
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
w(x1) = w
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x3, x5)
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
UNIF_LINESC_IN_GG(x1, x2) = UNIF_LINESC_IN_GG(x1, x2)
PD_IN_GGGGGG(x1, x2, x3, x4, x5, x6) = PD_IN_GGGGGG(x1, x2, x3, x4, x5, x6)
U21_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U21_GGGGGG(x1, x2, x3, x4, x5, x6, x7)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)
PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))

The TRS R consists of the following rules:

unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)
PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))

The TRS R consists of the following rules:

unif_pairscG_in_gg(w, .(w, X2)) → U44_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
unif_pairscG_in_gg(black, .(w, X2)) → U46_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(w, .(black, X2)) → U47_gg(X2, unif_pairscE_in_g(X2))
U44_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(w, X2))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
U46_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w, X2))
U47_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(black, X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w, .(w, X2))) → U36_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w, X2))) → U38_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w, .(black, X2))) → U39_g(X2, unif_pairscE_in_g(X2))
U36_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(w, X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U38_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w, X2)))
U39_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(black, X2)))

The set Q consists of the following terms:

unif_pairscG_in_gg(x0, x1)
U44_gg(x0, x1)
U45_gg(x0, x1)
U46_gg(x0, x1)
U47_gg(x0, x1)
unif_pairscE_in_g(x0)
U36_g(x0, x1)
U37_g(x0, x1)
U38_g(x0, x1)
U39_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

UNIF_LINESC_IN_GG(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → PD_IN_GGGGGG(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(PD_IN_GGGGGG(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₆
POL(U21_GGGGGG(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 1 + x₆
POL(U36_g(x₁, x₂)) = 0
POL(U37_g(x₁, x₂)) = 0
POL(U38_g(x₁, x₂)) = 0
POL(U39_g(x₁, x₂)) = 0
POL(U44_gg(x₁, x₂)) = 0
POL(U45_gg(x₁, x₂)) = 0
POL(U46_gg(x₁, x₂)) = 0
POL(U47_gg(x₁, x₂)) = 0
POL(UNIF_LINESC_IN_GG(x₁, x₂)) = x₂
POL([]) = 0
POL(black) = 0
POL(unif_pairscE_in_g(x₁)) = 0
POL(unif_pairscE_out_g(x₁)) = 0
POL(unif_pairscG_in_gg(x₁, x₂)) = 0
POL(unif_pairscG_out_gg(x₁, x₂)) = 0
POL(w) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PD_IN_GGGGGG(X1, X2, X3, X4, X5, X6) → U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U21_GGGGGG(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → UNIF_LINESC_IN_GG(.(X3, X4), .(X5, X6))

The TRS R consists of the following rules:

unif_pairscG_in_gg(w, .(w, X2)) → U44_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
unif_pairscG_in_gg(black, .(w, X2)) → U46_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(w, .(black, X2)) → U47_gg(X2, unif_pairscE_in_g(X2))
U44_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(w, X2))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
U46_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w, X2))
U47_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(black, X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w, .(w, X2))) → U36_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w, X2))) → U38_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w, .(black, X2))) → U39_g(X2, unif_pairscE_in_g(X2))
U36_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(w, X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U38_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w, X2)))
U39_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(black, X2)))

The set Q consists of the following terms:

unif_pairscG_in_gg(x0, x1)
U44_gg(x0, x1)
U45_gg(x0, x1)
U46_gg(x0, x1)
U47_gg(x0, x1)
unif_pairscE_in_g(x0)
U36_g(x0, x1)
U37_g(x0, x1)
U38_g(x0, x1)
U39_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(24) TRUE

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatcA_in_ga(x1, x2) = varmatcA_in_ga(x1)
[] = []
varmatcA_out_ga(x1, x2) = varmatcA_out_ga(x1, x2)
U29_ga(x1, x2, x3, x4, x5) = U29_ga(x1, x2, x5)
black = black
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
white = white
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
w(x1) = w
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x3, x5)
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
UNIF_MATRXB_IN_GG(x1, x2) = UNIF_MATRXB_IN_GG(x1, x2)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(26) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(27) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)

The TRS R consists of the following rules:

unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
black = black
w(x1) = w
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
UNIF_MATRXB_IN_GG(x1, x2) = UNIF_MATRXB_IN_GG(x1, x2)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(28) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)

The TRS R consists of the following rules:

unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_pairscG_in_gg(w, .(w, X2)) → U44_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
unif_pairscG_in_gg(black, .(w, X2)) → U46_gg(X2, unif_pairscE_in_g(X2))
unif_pairscG_in_gg(w, .(black, X2)) → U47_gg(X2, unif_pairscE_in_g(X2))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U44_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(w, X2))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
U46_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w, X2))
U47_gg(X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w, .(black, X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w, .(w, X2))) → U36_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w, X2))) → U38_g(X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w, .(black, X2))) → U39_g(X2, unif_pairscE_in_g(X2))
U36_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(w, X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U38_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w, X2)))
U39_g(X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w, .(black, X2)))

The set Q consists of the following terms:

unif_linescC_in_gg(x0, x1)
U35_gg(x0, x1, x2, x3, x4, x5, x6)
qcD_in_gggggg(x0, x1, x2, x3, x4, x5)
U42_gggggg(x0, x1, x2, x3, x4, x5, x6)
unif_pairscG_in_gg(x0, x1)
U43_gggggg(x0, x1, x2, x3, x4, x5, x6)
U44_gg(x0, x1)
U45_gg(x0, x1)
U46_gg(x0, x1)
U47_gg(x0, x1)
unif_pairscE_in_g(x0)
U36_g(x0, x1)
U37_g(x0, x1)
U38_g(x0, x1)
U39_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(30) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U7_GG(X1, X2, X3, unif_linescC_out_gg(X1, X2)) → UNIF_MATRXB_IN_GG(X2, X3)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
UNIF_MATRXB_IN_GG(X1, .(X2, X3)) → U7_GG(X1, X2, X3, unif_linescC_in_gg(X1, X2))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(31) YES

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U2_GA(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2, X4)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → VARMATA_IN_GA(X1, X3)
VARMATA_IN_GA(.(black, X1), .(black, X2)) → VARMATA_IN_GA(X1, X2)
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → VARMATA_IN_GA(X1, X3)

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))
unif_pairscG_in_gg(w(X1), .(w(X1), X2)) → U44_gg(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g([]) → unif_pairscE_out_g([])
unif_pairscE_in_g(.(w(X1), .(w(X1), X2))) → U36_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(black, .(black, X1))) → U37_g(X1, unif_pairscE_in_g(X1))
unif_pairscE_in_g(.(black, .(w(X1), X2))) → U38_g(X1, X2, unif_pairscE_in_g(X2))
unif_pairscE_in_g(.(w(X1), .(black, X2))) → U39_g(X1, X2, unif_pairscE_in_g(X2))
U39_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(black, X2)))
U38_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(black, .(w(X1), X2)))
U37_g(X1, unif_pairscE_out_g(X1)) → unif_pairscE_out_g(.(black, .(black, X1)))
U36_g(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscE_out_g(.(w(X1), .(w(X1), X2)))
U44_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(w(X1), X2))
unif_pairscG_in_gg(black, .(black, X1)) → U45_gg(X1, unif_pairscE_in_g(X1))
U45_gg(X1, unif_pairscE_out_g(X1)) → unif_pairscG_out_gg(black, .(black, X1))
unif_pairscG_in_gg(black, .(w(X1), X2)) → U46_gg(X1, X2, unif_pairscE_in_g(X2))
U46_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(black, .(w(X1), X2))
unif_pairscG_in_gg(w(X1), .(black, X2)) → U47_gg(X1, X2, unif_pairscE_in_g(X2))
U47_gg(X1, X2, unif_pairscE_out_g(X2)) → unif_pairscG_out_gg(w(X1), .(black, X2))
unif_linescC_in_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6))) → U35_gg(X1, X2, X3, X4, X5, X6, qcD_in_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6))
qcD_in_gggggg(X1, X2, X3, X4, X5, X6) → U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_in_gg(X1, X2))
U42_gggggg(X1, X2, X3, X4, X5, X6, unif_pairscG_out_gg(X1, X2)) → U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_in_gg(.(X3, X4), .(X5, X6)))
unif_linescC_in_gg(.(X1, []), .(X2, [])) → unif_linescC_out_gg(.(X1, []), .(X2, []))
U43_gggggg(X1, X2, X3, X4, X5, X6, unif_linescC_out_gg(.(X3, X4), .(X5, X6))) → qcD_out_gggggg(X1, X2, X3, X4, X5, X6)
U35_gg(X1, X2, X3, X4, X5, X6, qcD_out_gggggg(X1, .(X2, .(X4, .(X5, .(X1, .(X4, .(X2, .(X5, .(X1, .(X5, .(X2, .(X4, []))))))))))), X2, X3, X5, X6)) → unif_linescC_out_gg(.(X1, .(X2, X3)), .(X4, .(X5, X6)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatcA_in_ga(x1, x2) = varmatcA_in_ga(x1)
[] = []
varmatcA_out_ga(x1, x2) = varmatcA_out_ga(x1, x2)
U29_ga(x1, x2, x3, x4, x5) = U29_ga(x1, x2, x5)
black = black
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
white = white
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
w(x1) = w
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x3, x5)
unif_pairscG_in_gg(x1, x2) = unif_pairscG_in_gg(x1, x2)
U44_gg(x1, x2, x3) = U44_gg(x2, x3)
unif_pairscE_in_g(x1) = unif_pairscE_in_g(x1)
unif_pairscE_out_g(x1) = unif_pairscE_out_g(x1)
U36_g(x1, x2, x3) = U36_g(x2, x3)
U37_g(x1, x2) = U37_g(x1, x2)
U38_g(x1, x2, x3) = U38_g(x2, x3)
U39_g(x1, x2, x3) = U39_g(x2, x3)
unif_pairscG_out_gg(x1, x2) = unif_pairscG_out_gg(x1, x2)
U45_gg(x1, x2) = U45_gg(x1, x2)
U46_gg(x1, x2, x3) = U46_gg(x2, x3)
U47_gg(x1, x2, x3) = U47_gg(x2, x3)
unif_linescC_in_gg(x1, x2) = unif_linescC_in_gg(x1, x2)
U35_gg(x1, x2, x3, x4, x5, x6, x7) = U35_gg(x1, x2, x3, x4, x5, x6, x7)
qcD_in_gggggg(x1, x2, x3, x4, x5, x6) = qcD_in_gggggg(x1, x2, x3, x4, x5, x6)
U42_gggggg(x1, x2, x3, x4, x5, x6, x7) = U42_gggggg(x1, x2, x3, x4, x5, x6, x7)
U43_gggggg(x1, x2, x3, x4, x5, x6, x7) = U43_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linescC_out_gg(x1, x2) = unif_linescC_out_gg(x1, x2)
qcD_out_gggggg(x1, x2, x3, x4, x5, x6) = qcD_out_gggggg(x1, x2, x3, x4, x5, x6)
VARMATA_IN_GA(x1, x2) = VARMATA_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x5)

We have to consider all (P,R,Pi)-chains

(33) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(34) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → U2_GA(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
U2_GA(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2, X4)
VARMATA_IN_GA(.(X1, X2), .(X3, X4)) → VARMATA_IN_GA(X1, X3)
VARMATA_IN_GA(.(black, X1), .(black, X2)) → VARMATA_IN_GA(X1, X2)
VARMATA_IN_GA(.(white, X1), .(w(X2), X3)) → VARMATA_IN_GA(X1, X3)

The TRS R consists of the following rules:

varmatcA_in_ga([], []) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2), .(X3, X4)) → U29_ga(X1, X2, X3, X4, varmatcA_in_ga(X1, X3))
varmatcA_in_ga(.(black, X1), .(black, X2)) → U31_ga(X1, X2, varmatcA_in_ga(X1, X2))
varmatcA_in_ga(.(white, X1), .(w(X2), X3)) → U32_ga(X1, X2, X3, varmatcA_in_ga(X1, X3))
U29_ga(X1, X2, X3, X4, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, X4, varmatcA_in_ga(X2, X4))
U31_ga(X1, X2, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U32_ga(X1, X2, X3, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w(X2), X3))
U30_ga(X1, X2, X3, X4, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))

(35) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

VARMATA_IN_GA(.(X1, X2)) → U2_GA(X1, X2, varmatcA_in_ga(X1))
U2_GA(X1, X2, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2)
VARMATA_IN_GA(.(X1, X2)) → VARMATA_IN_GA(X1)
VARMATA_IN_GA(.(black, X1)) → VARMATA_IN_GA(X1)
VARMATA_IN_GA(.(white, X1)) → VARMATA_IN_GA(X1)

The TRS R consists of the following rules:

varmatcA_in_ga([]) → varmatcA_out_ga([], [])
varmatcA_in_ga(.(X1, X2)) → U29_ga(X1, X2, varmatcA_in_ga(X1))
varmatcA_in_ga(.(black, X1)) → U31_ga(X1, varmatcA_in_ga(X1))
varmatcA_in_ga(.(white, X1)) → U32_ga(X1, varmatcA_in_ga(X1))
U29_ga(X1, X2, varmatcA_out_ga(X1, X3)) → U30_ga(X1, X2, X3, varmatcA_in_ga(X2))
U31_ga(X1, varmatcA_out_ga(X1, X2)) → varmatcA_out_ga(.(black, X1), .(black, X2))
U32_ga(X1, varmatcA_out_ga(X1, X3)) → varmatcA_out_ga(.(white, X1), .(w, X3))
U30_ga(X1, X2, X3, varmatcA_out_ga(X2, X4)) → varmatcA_out_ga(.(X1, X2), .(X3, X4))

The set Q consists of the following terms:

varmatcA_in_ga(x0)
U29_ga(x0, x1, x2)
U31_ga(x0, x1)
U32_ga(x0, x1)
U30_ga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(37) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GA(X1, X2, varmatcA_out_ga(X1, X3)) → VARMATA_IN_GA(X2)
The graph contains the following edges 2 >= 1
VARMATA_IN_GA(.(X1, X2)) → U2_GA(X1, X2, varmatcA_in_ga(X1))
The graph contains the following edges 1 > 1, 1 > 2
VARMATA_IN_GA(.(X1, X2)) → VARMATA_IN_GA(X1)
The graph contains the following edges 1 > 1
VARMATA_IN_GA(.(black, X1)) → VARMATA_IN_GA(X1)
The graph contains the following edges 1 > 1
VARMATA_IN_GA(.(white, X1)) → VARMATA_IN_GA(X1)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

(4) Obligation:

(5) TriplesToPiDPProof (SOUND transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) DependencyGraphProof (EQUIVALENT transformation)

(24) TRUE

(25) Obligation:

(26) UsableRulesProof (EQUIVALENT transformation)

(27) Obligation:

(28) PiDPToQDPProof (SOUND transformation)

(29) Obligation:

(30) QDPSizeChangeProof (EQUIVALENT transformation)

(31) YES

(32) Obligation:

(33) UsableRulesProof (EQUIVALENT transformation)

(34) Obligation:

(35) PiDPToQDPProof (SOUND transformation)

(36) Obligation:

(37) QDPSizeChangeProof (EQUIVALENT transformation)

(38) YES